In this section we prove that the main forms of strong bisimilarity
for higher-order process calculi
coincide in \ahopi, and that such a  relation is
decidable.  As a key ingredient for our results, we introduce \emph{open Input/Output (IO) bisimulations} in which the variable of input prefixes is never
instantiated and $\tau$-transitions are not observed. 
To the best of our knowledge, \ahopi is the first calculus where IO bisimulation is discriminating 
enough to provide a useful characterization of process behavior.

%\iflong{}{Proofs  are sketched in Appendix~\ref{a:bism}.}
We define different kinds of bisimulations by appropriate combinations of the
clauses below.
%We write $m . P$ for $\inp m x . P$, if $ x \not \in \fv P$.

\begin{mydefi}[\ahopi\ bisimulation clauses, open processes]
\label{d:cla_op}
A symmetric relation $\R$   on \ahopi\ processes is
\begin{enumerate}
\item
% A relation $\R$   on \ahopi\ processes is
 a \emph{$\tau$-bisimulation} if $P
\RR Q$  and  $ P \arr{\tau}  {P'}$ imply that there is $Q'$ such that\ $ Q 
 \arr{\tau} {Q'}$ and ${P'} 
 \RR{Q'}$;

\item 
 a \emph{higher-order output  bisimulation}
if $P
\RR Q$  and 
 $ P \arr{\out a {P''}}  {P'}$ 
imply that there are $Q',Q''$ such that\ 
 $ Q 
 \arr{\out a {Q''}} {Q'}$ with ${P'} 
 \RR{Q'}$ and  ${P''} 
 \RR{Q''}$; 
\item 
 an \emph{output normal  bisimulation}
if $P
\RR Q$  and 
 $ P \arr{\out a {P''}}  {P'}$ 
imply that there are $Q',Q''$ such that\ 
$ Q 
 \arr{\out a {Q''}} {Q'}$ with ${ m . P''\parallel P'} 
 \RR{ m.Q'' \parallel Q'}$, where $m$ is fresh. 



\item an \emph{open} bisimulation   
if whenever $P
\RR Q$:
\begin{itemize}
\item
 $ P \arr{\inp a x}  {P'}$ 
implies that there is $Q'$ such that\
 $ Q 
 \arr{\inp a x} {Q'}$ and ${P'} 
 \RR{Q'}$, 
 

\item 
 $P \equiv x \parallel P'$ implies that there is $Q'$ such that\
 $Q \equiv x \parallel Q'$ and $P' \RR Q'$.
\end{itemize}
 

\end{enumerate}
\end{mydefi} 

\begin{mydefi}[\ahopi\ bisimulation clauses, closed processes]
\label{d:cla_clo}
A symmetric relation $\R$   on closed \ahopi\ processes  is
\begin{enumerate}
\item
 an \emph{output context bisimulation} 
if $P
\RR Q$  and 
 $ P \arr{\out a {P''}}  {P'}$ 
imply that there are $Q',Q''$ such that\ 
 $ Q 
 \arr{\out a {Q''}} {Q'}$ and for all $S$ with $\fv S \subseteq x$, it 
 holds that  $S \sub {P''} x \parallel P' 
 \RR S \sub {Q''} x \parallel Q'$;


 
\item 
 an \emph{input normal  bisimulation}
if $P
\RR Q$  and 
$ P \arr{\inp a x}  {P'}$
imply that there is $Q'$ such that\ 
$ Q 
 \arr{\inp a x} {Q'}$ and ${P'} \sub {\out m \nil}x 
 \RR{Q'}\sub {\out m\nil}x$, where $m$ is fresh;
 



\item 
\emph{closed} if 
 $P
\RR Q$  and 
$ P \arr{\inp a x}  {P'}$
imply that there is $Q'$ such that\ 
$ Q 
 \arr{\inp a x} {Q'}$ and for all closed  $R$,  it holds that ${P'\sub Rx} 
 \RR{Q'\sub Rx}$. 
\end{enumerate}
\end{mydefi} 

A combination of the 
%\ahopi\ 
bisimulation clauses in
Definitions~\ref{d:cla_op} and \ref{d:cla_clo} is
 \emph{complete}
if it includes   exactly one   clause for input and
output transitions (in contrast, it need not include a clause for
$\tau$-transitions).\footnote{The clauses of Definition~\ref{d:cla_clo} are however
  tailored to closed processes, therefore combining them with 
clause 4 in 
%the open clause of 
Definition~\ref{d:cla_op} %(4) 
has little interest.}
We will show that all complete combinations
 coincide. 
We only give a name to %some of the combinations --- 
those 
combinations
that represent
known forms of bisimulation for higher-order processes or that  are
needed in our proofs.
In each case,
as usual, a \emph{bisimilarity}  is the union of all bisimulations,
and is itself a bisimulation 
 (the functions from
relations to relations that represent the 
  bisimulation clauses in  Definitions~\ref{d:cla_op} and \ref{d:cla_clo} are
all monotonic).


\begin{mydefi}
\label{d:bisimulations}
%\begin{itemize}
%\item 
\emph{Higher-order bisimilarity}, written $\simHO$, is the 
largest relation on 
closed \ahopi\ processes
that is  a
  $\tau$-bisimulation, a higher-order output bisimulation, and is
  closed. 
 
%\item 
\emph{Context bisimilarity}, written $\simCON$, is the 
largest relation on 
closed \ahopi\ processes
that is  a
  $\tau$-bisimulation, an  output  context bisimulation, and is
  closed. 


%\item 
\emph{Normal bisimilarity}, written $\simNOR$, is the 
largest relation on 
closed 
\ahopi\ processes
that is  a
  $\tau$-bisimulation, an  
output  normal bisimulation, and an
input
normal bisimulation.

%, and is   closed. 


%\item  
\emph{IO bisimilarity},  
written $\simIOo$, is the 
largest relation on 
 \ahopi\ processes
that is
  a higher-order output bisimulation and is
open. 

%\item  
\emph{Open normal bisimilarity},  
written $\simNORo$, is the 
largest relation on 
 \ahopi\ processes
that is
a  $\tau$-bisimulation,  an  output normal bisimulation, and is
open. 
%\end{itemize}
 \end{mydefi} 






%A bisimilarity on closed processes is extended to
%open processes by  closing under substitutions; for instance
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  #1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%\iflong{if $\fv {P,Q} \subseteq {\tilX}$ then $P \simCON  Q$  
%if for all closed ${\til R}$, we have 
%$P{\sub {\til R}\tilX} \simCON Q{\sub {\til R}\tilX}$.
%}{ 
%if $\fv {P,Q} \subseteq \{x_1, \ldots, x_n\}$ then $P \simCON  Q$  
%if for all closed $R_1, \ldots, R_n$, we have $P \{\suba{R_1}{x_1}, \ldots, \suba{R_n}{x_n}\} \simCON 
%Q \{\suba{R_1}{x_1}, \ldots, \suba{R_n}{x_n}\}$.
%}

{\em Environmental bisimilarity} \citep{SangiorgiKS07},
a recent proposal of bisimilarity for higher-order calculi,
 in \ahopi
roughly corresponds to (and indeed coincides with)
 the complete combination that is
a $\tau$-bisimulation, an output normal bisimulation, and is closed.



\begin{remark}
%\label{r:} 
%{\em 
The input clause of Definition~\ref{d:cla_clo}(3)
is in the \emph{late} style. It is known \citep{San923} that in calculi of pure
higher-order concurrency  early and late clauses are equivalent.
%}
\end{remark} 

\begin{remark}
%\label{r:} 
% {\em 
In contrast with ordinary normal bisimulation \citep{San923,JR05},
our clause for output normal bisimulation does not use a replication
in front of the introduced fresh name. 
Such a replication would be  needed in extensions of  the calculus
(e.g.,  with recursion or restriction).
%  but, as we will show,  is not needed in
% \ahopi.
% }
\end{remark} 

\iflong{
A bisimilarity on closed processes is extended to open processes as follows.
\begin{mydefi}[Extension of bisimilarities]
\label{d:extbis}
Let $\R$ be a bisimilarity on closed \ahopi processes. 
The extension of $\R$ to open \ahopi processes is defined by
$$
\R^{\tt o} = \{(P,Q):\, a(x_1).\cdots.a(x_n).P\, \R\, a(x_1).\cdots.a(x_n).Q \} 
$$
where $\fv {P} \cup \fv{Q} = \{x_1, \ldots, x_n\}$, and $a$ is fresh in $P,Q$.
\end{mydefi}}{Given a bisimilarity 
$\R$
on closed processes, its 
extension to open processes is 
%the relation with all pairs of the form 
%\[(a(x_1).\cdots.a(x_n).P,\, a(x_1).\cdots.a(x_n).Q) \]
%where $\fv {P,Q} = \{x_1, \ldots, x_n\}$, and  $a$ is fresh in $P,Q$.
defined by
\[ \{(P,Q):\, a(x_1).\cdots.a(x_n).P\, \R\, a(x_1).\cdots.a(x_n).Q \} \]
with $\fv {P} \cup \fv{Q} = \{x_1, \ldots, x_n\}$, and  $a$ fresh in $P,Q$.
}

The simplest  complete form of bisimilarity  is $\simIOo$. Not only $\simIOo$ is
the less demanding for proofs; it also has  a straightforward proof of
congruence. This is significant because congruence is a notoriously
hard problem in bisimilarities for higher-order calculi. 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  #2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\iflong{Before describing the proof of congruence for $\simIOo$, we first define an 
auxiliary up-to technique that will be useful later.

\begin{mydefi}
\label{d:upto}
A symmetric relation $\RR$ on {\PrOp} is an \emph{open IO bisimulation up-to $\equiv$}  if 
 $ P\RR Q   $ implies:
\begin{enumerate}
\item if $ P \arr{\inp a x}  {P'}$ then $ Q
 \arr{\inp a x} {Q'}$ and ${P'} \equiv \RR \equiv {Q'}$;

\item if $ P \arr{\out a {P''}}  {P'}$ then $ Q
 \arr{\out a {Q''}} {Q'}$ with ${P'} \equiv  \RR \equiv {Q'}$ and  ${P''} \equiv  \RR \equiv {Q''}$;

\item if $P \equiv x \parallel P'$ then  $Q \equiv x \parallel Q'$ and $P' \equiv \RR \equiv Q'$.
%\item the converse of the 3 clauses above, with $Q$ making the   challenge.
\end{enumerate}
% We write $P \simIOo Q $ if $P\RR Q$ for some open IO bisimulation $\R$. 
\end{mydefi}

\begin{lemma}
\label{l:upto}
If $\RR$ is an open IO bisimulation up-to $\equiv$ and $(P,Q) \in\ \RR$ then $P \simIOo Q$.
%If $\RR$ is an open IO bisimulation up-to $\equiv$ then $\RR \subseteq \simIOo$.
\end{lemma}
\begin{proof}
The proof proceeds by a standard diagram-chasing argument (as in, e.g., \citep{Milner89}): 
using Lemma \ref{l:equiv} one shows that $\equiv \RR\ \equiv$ is a $\simIOo$-bisimulation.
%, and by transitivity of $\equiv$ then the result follows.
\end{proof}
%}{
%}

We now give the congruence result for $\simIOo$.
%\iflong{
\begin{lemma}[Congruence of $\simIOo$]
\label{l:simIOo_cong} 
Let $P_1,P_2$ be open \ahopi processes. $P_1 \simIOo P_2$ implies:
\begin{enumerate}
\item $a(x).P_1 \simIOo a(x).P_2$
\item $P_1 \parallel R \simIOo P_2 \parallel R$, for every $R$
\item $\overline{a}\langle P_1 \rangle \simIOo \overline{a}\langle P_2 \rangle$
%\item $x \parallel P_1  \simIOo x \parallel P_2$
\end{enumerate}
\end{lemma}
\begin{proof}
Items (1) and (3) are straightforward by showing the appropriate $\simIOo$-bi\-si\-mu\-la\-tions. 
We consider only (2). We show that, for every $R$, $P_1$, and $P_2$
\[
\S = \{(P_1 \parallel R,\, P_2 \parallel R)~:~P_1 \simIOo P_2\}
\]
is a $\simIOo$-bisimulation. 
We first suppose $P_1 \parallel R \arr{\alpha} P'$; 
we need to find a matching action from $P_2 \parallel R$. 
We proceed by case analysis on the rule used to infer $\alpha$. 
There are two cases. 
In the first one $P_1 \arr{\alpha} P'_1$ and $P' = P'_1 \parallel R$ is inferred 
using rule \textsc{Act1} (by $\alpha$-conversion we can ensure that $R$ respects 
the side condition of the rule). 
By definition of $\simIOo$-bisimulation, $P_2 \arr{\alpha} P'_2$ with 
$P'_1 \simIOo P'_2$. 
Using rule \textsc{Act1} we infer that also
$P_2 \parallel R \arr{\alpha} P'_2 \parallel R$.
We conclude that $(P'_1 \parallel R, P'_2 \parallel R) \in \S$.
The second case follows by an analogous argument and occurs when 
$R \arr{\alpha} R'$ so that $P' = P_1 \parallel R'$  by rule \textsc{Act2}. 

The last thing to consider is when
%Notice that by definition of $\simIOo$ it could be that
$P_1 \parallel R \equiv x \parallel P'$; we need to show that $P_2 \parallel R \equiv x \parallel Q'$ and that 
$(P',Q') \in \S$. We distinguish two cases, depending on the shape of $P'$. 
First, assume that $P' \equiv P_1' \parallel R$, that is,
$x$ is a subprocess of $P_1$. Since $P_1 \simIOo P_2$, then it must be that 
$P_2 \equiv x \parallel P'_2$ for some $P'_2$, with $P'_1 \simIOo P'_2$.
Taking $Q' \equiv P'_2 \parallel R$ we thus have $(P',Q') \in \S$. 
Second, assume $x$ is a subprocess of $R$, and we have $P' \equiv P_1 \parallel R'$, we then take
$Q' \equiv P_2 \parallel R'$. Since $\S$ is defined over every $R$, then $(P',Q') \in \S$.
\end{proof}}{
\begin{lemma} 
\label{l:simIOo_cong} 
$\simIOo$ is a congruence relation. 
\end{lemma}
\begin{proof}[Proof (Sketch)]
By showing that $\simIOo$ is preserved by each operator of the calculus. 
All cases are  easy. For parallel composition, it is essential that $\simIOo$ 
does not require to match $\tau$ actions in the bisimulation game. 
% For input 
% prefix, the open style makes the reasoning particularly easy. 
\end{proof}
}




\begin{lemma}[$\simIOo$  is preserved by substitutions]
\label{l:simIOo_sub}
If  $P \simIOo Q$ then for all $x$ and $R$, also  
$P \sub R x \simIOo Q\sub Rx$. 
\end{lemma}  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  #3
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
\iflong{
\begin{proof}[Proof] 
We show that, for processes $P,Q$ in which $x$ is guarded, 
\[\RR\ = \{(P\sub Rx \parallel L,\, Q\sub Rx \parallel L )~:~ P \simIOo Q\} \] %\quad \mbox{($P,Q$ are guarded)}\]
%where $P,Q$ are guarded and  . We show that this 
is a $\simIOo$-bisimulation up-to $\equiv$ (Definition \ref{d:upto}). (This suffices, because of Lemma \ref{l:upto}.)
Consider a pair $(P\sub Rx \parallel L,\, Q\sub Rx \parallel L ) \in\ \RR$.
We shall concentrate on the possible moves from 
$P\sub Rx$, say $P\sub Rx\arr \alpha P'$; transitions from $L$, if any, can be handled analogously.
We  proceed by case analysis on the rule used to infer $\alpha$.

We only detail the case in which $\alpha $ is an input action $a(x)$ inferred using rule \textsc{Inp};
the case in which $\alpha$ is an output is similar (there may be a substitution on the label). 
%\as{Why not show the more complex case of output? Also, whatever case is chosen, instantiate the label accordingly.}
Since $x$ is guarded in $P$, using Lemma~\ref{l:GUA}(2),
%and \ref{l:equiv_cont}, 
%there is $\alpha_1 $ such that\ 
there is $P_1$ such that\ 
$P\arr {a(x)} P_1$ %with $\alpha = \alpha_1 \sub Rx$ 
and  $P' = P_1 \sub Rx$. By definition of $\simIOo$-bisimulation, also
$Q\arr {a(x)} Q_1$ with $P_1 \simIOo Q_1$.
Hence, by Lemma~\ref{l:GUA}(1), 
$Q \sub Rx \arr {a(x)} Q_1\sub Rx$. 
It remains to show that $P_1 \sub Rx$ and $Q_1\sub Rx$ can be
rewritten into the form  required in the bisimulation.
Using Lemma~\ref{l:equiv_cont}(1), we have 
\[ 
P_1  \equiv P_1' \parallel \prod^n x \quad \mbox{and} \quad Q_1  \equiv Q_1' \parallel \prod^m x 
 \]
for $P_1', Q'_1$ in which $x$ is guarded. As $P_1 \simIOo Q_1$, it must be $n=m$ and $P'_1 \simIOo Q'_1$.
Finally, using Lemmas~\ref{l:equiv_cont}(2) and \ref{l:simIOo_cong} we have
\[ 
P_1\sub Rx  \equiv P_1'\sub Rx \parallel \prod^n R  \quad \mbox{and} \quad Q_1\sub Rx  \equiv Q_1'\sub Rx \parallel \prod^n R %\parallel L
 \]
which closes up the bisimulation up-to $\equiv$. 
\end{proof}}{
\begin{proof}[Proof (Sketch)] 
We take the relation on $\PrOp$ with all pairs of the form 
\[(P'\sub Rx \parallel L,\, Q'\sub Rx \parallel L )   \] 
where $P',Q'$ are guarded (i.e., free variables occur only in
 sub-expressions of the form $\pi.S$, where $\pi$ is a prefix) and $P'
 \simIOo Q'$, and show that this is an open IO bisimulation up to
 $\equiv$ (this simple form of ``up-to technique'' is common for
 bisimilarities).  The proof makes use of 
lemmas showing the effect of process substitutions
 on  the behaviors of open processes, 
and of a few simple algebraic manipulations.
\end{proof}
}
 


The most striking property of $\simIOo$ is its decidability. 
In contrast with  the other bisimilarities, in $\simIOo$ the size of
 processes always decreases during
the bisimulation game. This 
%holds 
is
because $\simIOo$ is an open
relation and does not have a clause for $\tau$ transitions, hence
process copying never occurs. 


\begin{lemma}
\label{l:decIOo} 
Relation  $\simIOo$  is decidable.  
\end{lemma}
 



Next we show that $\simIOo$  is  also a $\tau$ bisimulation. This will
allow us to prove that $\simIOo$ coincides with other bisimilarities, and
to transfer to them its properties, in particular congruence
and decidability.



\begin{lemma}
\label{l:tauIOo}
Relation $ \simIOo$ is a $\tau$-bisimulation.
\end{lemma} 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  #4
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\iflong
{\begin{proof}[Proof]
%To show that relation $\simIOo$
%\[
%\SS\ = \{(P,\,Q)~:~ P \simIOo Q \}
%\]
%is a $\tau$-bisimulation.
Suppose  $(P,Q) \in\ \simIOo$ and $P \arr \tau P'$; we have to find a
matching transition $Q \arr \tau Q'$. 
Action $\tau$ was inferred using either rule \textsc{tau1} or \textsc{tau2}, so we have two cases. 
We consider only the first one as the second is analogous. 
If rule \textsc{Tau1} was used, then we can decompose $P$'s transition into an output 
$P \arr{\out a R} P_1$ followed by an input  $P_1 \arr{\inp a x } P_2$, 
with $P' = P_2 \sub R x$
(that is, the structure of $P$ is $P \equiv \out a R \parallel a(x).P_2$).
By definition of $\simIOo$, $Q$ is capable of matching these two
transitions, and the final derivative is a process $Q_2$ with $Q_2 \simIOo P_2$. 
Further, as \ahopi\ has no output prefixes (i.e., it is  an  asynchronous calculus) 
the two transitions from $Q$ can be  combined into a $\tau$-transition. Finally, 
since $\simIOo$ 
%is a congruence (Lemma~\ref{l:simIOo_cong}) and 
is preserved by substitutions (Lemma \ref{l:simIOo_sub}), we can use 
rule \textsc{Tau1} to derive a process $Q' =  Q_2 \sub R x$ that  
matches the $\tau$-transition from $P$, with $(P', Q') \in\ \simIOo$.
\end{proof}
}{
\begin{proof}[Proof (Sketch)]
Suppose  $P \simIOo Q $ and  $P \arr \tau P'$. We have to find a
matching transition from $Q$. 
We can decompose $P$'s transition into an output 
 $P \arr{\out a R} P_1$ followed by an input   $P_1 
\arr{\inp a x } P_2$, with $P' = P_2 \sub R x$.
By definition of $\simIOo$, $Q$ is capable of matching these
transitions, and the final derivative
is a process $Q_2$ with $Q_2 \simIOo P_2$. 
 Further, as \ahopi\ has no output prefixes (i.e., it is  an
 asynchronous calculus) the two transitions from $Q$ can be
 combined into a $\tau$-transition, which matches the initial
 $\tau$-transition from $P$. We conclude using  
Lemmas~\ref{l:simIOo_cong}  and \ref{l:simIOo_sub}.
\end{proof}
}  


\begin{corollary}
\label{c:HO_IOo}
$\simHO$ and $\simIOo$ coincide. 
\end{corollary}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  #5
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\iflong
{\begin{proof}[Proof]
The hard implication is the one right to left ($\simIOo$ implies $\simHO$). One shows that 
for closed $P,Q$, $ \simIOo$
%\[
%\SS\ = \{(P,\,Q)~:~ P \simIOo Q \} %\qquad (P,Q \textrm{ are closed})
%\]
is a $\simHO$-bisimulation. Suppose $(P_1, P_2) \in\  \simIOo$ and $P_1 \arr{\alpha} Q_1$; 
we need to find a matching transition $P_2 \arr{\alpha} Q_2$.
%We proceed by case analysis on the action $\alpha$. 
We consider three cases, one for each form that $\alpha$ can take. 
Case $\alpha = \out a R$ is 
immediate as both $\simHO$ and $\simIOo$
are higher-order output bisimulations. 
As for cases  $\alpha = a(x)$ and  $\alpha = \tau$, 
the desired transition can be easily obtained using 
%For case $\alpha = a(x)$, we use 
Lemmas~\ref{l:simIOo_sub} ($\simIOo$ is preserved by substitutions) and 
%Finally, if $\alpha = \tau$ we apply 
%Lemma~
\ref{l:tauIOo} ($\simIOo$ is a $\tau$-bisimulation), respectively.
\end{proof}
}{
\begin{proof}[Proof (Sketch)]
The hard implication is the one right to left. One shows that 
$\simIOo$, 
restricted to
closed processes,
 is a higher-order bisimulation.
The clause for output actions is trivial (they are the same);  for inputs, we apply
Lemma~\ref{l:simIOo_sub}; for $\tau$ we apply Lemma~\ref{l:tauIOo}.
\end{proof}
}

We thus infer that $\simHO$ is a congruence 
relation. A direct proof of this result (by exhibiting an appropriate 
bisimulation), in particular congruence for 
parallel composition, would have been harder. 
Congruence of higher-order
bisimilarity is usually proved by appealing to, and adapting, 
Howe's method for the $\lambda$-calculus  \citep{howe}.
%  (also, the method works well in functional languages, but in
% concurrency can sometimes give problems). 



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  #6_0
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\iflong{
We now move to the relationship between $\simHO$, $\simNORo$, and $\simCON$.
We begin by establishing a few properties of normal bisimulation.
}{ 
For the remaining characterizations we
first establish
 a few properties
of normal bisimulation. 
}
 
\begin{lemma} 
\label{l:nor_deco} 
If $\inpC m . P_1 \parallel P \simNORo\inpC  m . Q_1 \parallel  Q$, for some fresh $m$,
% for $P_i,Q_i$ ($i=1,2$), 
then we have $P_1 \simNORo Q_1$ and  $P \simNORo Q$.
\end{lemma}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  #6 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\iflong
{
\begin{proof}
We show that, for any fresh names $m_1, \ldots $, 
\[
\SS\ = \bigcup^\infty_{j=1} \{(P,\,Q)~:~ 
%\inpC m_1.P_1 \parallel \cdots \parallel m_j.P_j \parallel P \simNORo
%\inpC m_1.Q_1 \parallel \cdots \parallel m_j.Q_j \parallel Q \} 
P  \parallel \prod_{k \in 1..j} \inpC m_k.P_k \simNORo
Q  \parallel \prod_{k \in 1..j} \inpC m_k.Q_k \} 
\]
%for $i =1,2$ and $m$ fresh, are 
%and 
\[
\SS_1 = \bigcup^\infty_{j=1} \{(P_1,\,Q_1)~:~ 
%\inpC m_1.P_1 \parallel \cdots \parallel m_j.P_j \parallel P \simNORo
%\inpC m_1.Q_1 \parallel \cdots \parallel m_j.Q_j \parallel Q \} 
P \parallel \prod_{k \in 1..j} \inpC m_k.P_k  \simNORo
Q \parallel \prod_{k \in 1..j} \inpC m_k.Q_k  \} 
\]
are $\simNORo$-bisimulations. %We show $P_1 \simNORo Q_1$ and $P_2 \simNORo Q_2$ separately.

We start with $\SS$. %\as{For this relation we probably need to extend the relation to any fresh name $m$, not just fix one.}
%First $P_2 \simNORo Q_2$. 
Suppose $(P,Q) \in \,\SS$ and that $P \arr \alpha P'$; we need to show 
a matching action from $Q$.
We have different cases depending on the shape of $\alpha$. We consider only the case $\alpha = \out a {P''}$, the others being simpler.
By \textsc{Act1} we have 
\[
%\inpC m_1 . P_1 \parallel \cdots \parallel m_j.P_j 
P \parallel \prod_{k \in 1..j} \inpC m_k.P_k 
 \arr{\out a {P''}} 
%\inpC  m_1 . P_1 \parallel \cdots \parallel m_j.P_j 
 P' \parallel \prod_{k \in 1..j} \inpC m_k.P_k.\] 
Since 
$ P \parallel \prod_{k \in 1..j} \inpC m_k.P_k 
\simNORo 
Q \parallel \prod_{k \in 1..j} \inpC m_k.Q_k  $,
there should exist a $Q^*$ such that 
\[ 
Q \parallel \prod_{k \in 1..j} \inpC m_k.Q_k 
%\inpC m_1.Q_1 \parallel \cdots \parallel m_j.Q_j  
\arr{\out a {Q''}}  Q^*\, ,\]
with %\as{Needs to be fixed from here: the actual relation we get depends on the label (for an output there is an extra process guarded by a fresh name).} 
$ P' \parallel \prod_{k \in 1..j} \inpC m_k.P_k 
\parallel m''.P'' \simNORo Q^* \parallel m''.Q''$. 
As $m_1, \ldots, m_j$ are fresh, they do not occur in $P$, thus $\out a {P''}$ does not mention them. 
For the same reason, there cannot be any communication between 
%$\inpC m_1 . Q_1 \parallel \cdots \parallel m_j.Q_j $ 
$\prod_{k \in 1..j} \inpC m_k.Q_k$
and $Q$;  
so,   we infer that the only possible transition is 
\[
 Q  \parallel \prod_{k \in 1..j} \inpC m_k.Q_k 
%\inpC m_1 . Q_1 \parallel \cdots \parallel m_j . Q_j 
 \arr{\out a {Q''}}  
Q^* = 
 Q' \parallel \prod_{k \in 1..j} \inpC m_k.Q_k 
%\inpC m_1 . Q_1 \parallel \cdots \parallel m_j.Q_j 
 ,\]
applying rule \textsc{Act1}  to $Q  \arr{\out a {Q''}}  Q'$.
Since $
P' \parallel \prod_{k \in 1..j} \inpC m_k.P_k 
\parallel  m''.P'' \simNORo
Q' \parallel \prod_{k \in 1..j} \inpC m_k.Q_k 
\parallel  m''.Q''$, 
we have $(P', Q') \in\ \SS$ as needed.

Before considering $\SS_1$, we find it useful to detail a procedure for \emph{consuming} $\simNORo$-bisimilar processes.
%We shall exploit it below as well as in the proof of Lemma \ref{l:abc}. 

Given a process $P$, let $o(P)$ denote the number of output actions in $P$. Let $m(P) = \size{P}+o(P)$
be the measure that considers both the (lexical) size of $P$  and the number of output actions in it.
Consider now two $\simNORo$-bisimilar processes $P$ and $Q$. The procedure consists in consuming one of them by performing its actions completely; 
the other process can match these actions (as it is $\simNORo$-bisimilar) and will be consumed as well.
We will show that $m(P)$ decreases at each step of the bisimulation game; at the end, we will  
obtain processes $P_n$ and $Q_n$ with $m(P_n) = m(Q_n) = 0$. 

To illustrate the procedure, suppose, w.l.o.g., process $P$ has the following shape: 
\[
P \equiv \prod_{h \in 1..t} x_h \parallel \prod_{i \in 1..k} a_i(x_i).P_i \parallel \prod_{j \in 1..l} \out {b_j} {P_j}
\]
where we have $t$ top-level variables, $k$ input actions, and $l$ output actions. 
We use $a_i$ and $b_j$ 
for channels in input and output actions, respectively.
The first step is to remove top-level variables; this relies on the fact  $\simNORo$ is an open bisimilarity. One thus obtains processes $P_1$ and $Q_1$ with only input and output actions, and both $m(P_1) < m(P)$ and $m(Q_1) < m(Q)$ hold. As a second step, the procedure exercises every output action in $P_1$. By definition of $\simNORo$, $Q_1$ should be able to match those actions. Call the resulting processes $P_2$ and $Q_2$. 
%By recalling that an output action implies the addition of a input process guarded by a fresh name, we notice that measures $m(P_2)$ and $m(Q_2)$ strictly decrease wrt $m(P_1)$ and $m(Q_1)$. \
Recall that when an output $\out a {P_j}$ is consumed in the bisimulation game, process $m_j.P_j$ is added in parallel.
Thus since $\size{\out a P_j} = \size{m_j.P_j}$ and the number of outputs decreases, measure $m$ decreases as well.
More precisely, one has that
\[
P_2 \equiv \prod_{i \in 1..k} a_i(x_i).P_i \parallel \prod_{j \in 1..l} m_j.P_j \]
%contains $k+l$ input prefixes (
where $m_j$ stands for a fresh name. Then, one has to consider the $k+l$ input actions in each process; their consumption proceeds as expected. One obtains processes $P_3$ and $Q_3$ that are bisimilar, with strictly decreasing measures for both processes. The procedure concludes by iterating the above steps on $P_3$ and $Q_3$. In fact, we have shown that at each step measure $m$ strictly decreases; this guarantees that eventually one will reach processes $P_n$ and $Q_n$, with $m(P_n) = m(Q_n) = 0$ as desired.

With the above procedure showing $\SS_1$ is a bisimulation is straightforward. Take the $\simNORo$-bisimilar processes 
$
P \parallel \prod_{k \in 1..j} \inpC m_k.P_k $ and 
$Q \parallel \prod_{k \in 1..j} \inpC m_k.Q_k $. 
Using the procedure above over $P$ and $Q$ we obtain 
$
\prod_{k \in 1..j} \inpC m_k.P_k \simNORo 
%\inpC m_1 . P_1 \parallel \cdots \parallel m_j.P_j 
\prod_{k \in 1..j} \inpC m_k.Q_k $.
%inpC  m_1.Q_1 \parallel \cdots \parallel m_j.Q_j$. 
This is because fresh names $m_1, \ldots, m_j$ do not occur in $P$ and $Q$, and hence they do not intervene in $P$ and $Q$'s consumption.
Similarly, we can consume $\prod_{{k'} \in 2..j} \inpC m_{k'}.P_{k'}$
(i.e. all the components excepting $m_1.P_1$) and the corresponding
$\prod_{{k'} \in 2..j} \inpC m_{k'}.Q_{k'}$.
We thus end up with $\inpC  m_1.P_1  \simNORo  \inpC  m_1.Q_1 $, 
and  we observe that the only possible action on each side is the input on $m_1$,
which can be trivially matched by the other. We then infer that $(P_1, Q_1) \in\, \SS_1$, as desired.
%Now we show $\SS_1$.
%%$P_1 \simNORo Q_1$. 
%We start by consuming every action of $P_2$. Suppose, w.l.o.g., that 
%\[
%P_2 \equiv \prod_{h \in 1..t} x_h \parallel \prod_{i \in 1..k} a_i(x_i).P_i \parallel \prod_{j \in 1..l} \out {b_j} {P_j}
%\]
%where we have $t$ top-level variables, $k$ input actions, and $l$ output actions. 
%We use $a_i$ and $b_j$ 
%for channels in input and output actions, respectively.
%%Further, let $T$ represent all the subprocesses capable of performing a $\tau$ action.
%Since $P_2 \simNORo Q_2$, we can assume a similar structure for $Q_2$. \as{As it's the first time we're seeing this kind of proof (and as it will happen again for other results, such as the asynchronous ones), I would detail more. I would describe the measure first (lexical order on size of the process (on the $P$ side) and number of available outputs (on the $P$ side)), then describe the procedure that shows goes down to the empty process (get rid of variables, get rid of output, get rid of input, repeat), showing everything always decreases. We don't need to show the processes have the same shape: when $P_2$ is completely consumed, it's equivalent to $0$, so the consumption of $Q$ has to be $0$ as well. And don't forget to argue each time why the $\inpC m . Q_1$ cannot participate in the matching of reductions from the $P_2$ side.}
%Notice that, by the definition of open bisimulation, we can disregard top-level variables so that we have 
%a subprocess of $P_2$ that only has input and output actions. Also by definition, 
%this subprocess of $P_2$ will be bisimilar to some analogous subprocess of $Q_2$.
%Now suppose every output action of this subprocess of $P_2$ is exercised;
%according to the definition of
%output normal bisimulation, we end up with a process
%$$P'_2 \equiv \prod_{i \in 1..k} a_i(x_i).P_i \parallel \prod_{j \in 1..l} m_j.P_j$$
%that contains $k+l$ input prefixes, and where $m_j$ stands for a fresh name.
%By definition of $\simNORo$, $Q_2$ has also a subprocess without top-level variables and that can
%perform all these output actions as well, so evolving to a $Q'_2$ such that
%$P'_2 \simNORo Q'_2$. Again, we can consume each of the input actions in $P'_2$ and $Q'_2$, 
%leading to processes $P''_2$ and $Q''_2$ that are still $\simNORo$-bisimilar.
%Suppose we further consume actions in processes  $P''_2$ and $Q''_2$, in such a way that 
%they remain $\simNORo$-bisimilar. 
%When an input action is consumed the size of the process strictly decreases; when an output is performed
%the size of the process remains unchanged and the number of output actions strictly decreases. 
%Thus, the size of 
%% while their size strictly decreases; 
%%indeed, by noting that the size of a term strictly decreases when an action is consumed 
%%one can show that the size of 
%$P''_2$ and $Q''_2$ will  eventually be zero.
%Once that occurs, we have $\inpC m . P_1  \simNORo \inpC m . Q_1 $, 
%and  we observe that the only possible action on each side is the input on $m$,
%which can be trivially matched by the other. We then infer that $P_1$ should be bisimilar to $Q_1$.
\end{proof}


\begin{lemma}
\label{l:HO_CON}
$\simHO$ implies $\simCON$.
\end{lemma}
%\iflong{
\begin{proof}
%We show that the relation $ \simHO$
%\[
%\RR = \{(P,Q)~:~P \simHO Q\}
%\]
%is a $\simCON$-bisimulation. \
We suppose $(P,Q) \in\ \simHO$ and $P \arr \alpha P'$; we need to show
a matching action from $Q$. We proceed by case analysis on the form $\alpha$ can take. 
The only interesting case is when $\alpha$ is a higher-order output; the remaining clauses are the same
in both relations. By definition of $\simHO$, if $P \arr{\out a {P''}} P'$ 
then $Q \arr{ \out a { Q''}} Q'$, with 
both $P'' \simHO Q''$ and $P' \simHO Q'$.
We need to show that, for every $S$ such that $\fv S = \{x\}$, 
$S \sub {P''} x \parallel P' \simHO S \sub {Q''} x \parallel Q'$; this follows from 
$P'' \simHO Q''$ and $P' \simHO Q'$ and the fact that $\simHO$ is both a congruence and preserved by
substitutions.
\end{proof}

\begin{lemma}
\label{l:CON_NOR}
$\simCON$ implies $\simNOR$.
\end{lemma}
\begin{proof}
Straightforward by showing an appropriate bisimulation. The result is immediate
by noticing that 
(i) both relations are $\tau$-bisimulations, and that (ii)
the input and output clauses of $\simNOR$ are instances of those of $\simCON$.
In the output case, by selecting a process $S = \inpC m . x$ (with $m$ fresh) one obtains the 
desired form for the clause. The input clause is similar, and follows from the definition
of closed bisimulation, which holds for every closed process $R$; in particular, it also holds for 
$R = \out m \nil$ (with $m$ fresh) as required by the clause of $\simNOR$.
\end{proof}


\begin{lemma} 
\label{l:norOpCl} 
%Normal bisimilarity and open normal bisimilarity coincide. 
$\simNOR$ implies $\simNORo$.
\end{lemma}  
%}{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  #7
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%%%%%\iflong{
\begin{proof}
We consider open processes, and as such, in what follows 
we consider the extension of $\simNOR$ to open processes as in Definition \ref{d:bisimulations}, which 
we denote  $\simNORex$. 
Notice that since $\simNOR$ is an input normal bisimulation (Definition \ref{d:cla_clo}(2)), 
$\simNORex$ can be equivalently defined as 
$$ 
P \simNORex Q \mbox{ iff } P \{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \} \simNOR 
Q \{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \}
$$
where $\{x_1, \ldots, x_n \} = \fv{P} \cup \fv{Q}$ and $m_1, \ldots, m_n$ are fresh names. 
We will show that $\simNORex$ is an open normal bisimulation.

We first suppose $P \simNORex Q$ and $P \arr \alpha P'$;
we need to find a matching transition $Q \arr \alpha Q'$. 
We perform a case analysis on the shape $\alpha$ can take. 
In all cases, one uses the definition of $\simNORex$ to show that the desired transition actually takes place.
Next, we only detail the case in which $\alpha = a(x)$, so we 
%The interesting case is the input $\alpha = a(x)$; cases for $\tau$ and output actions
%are immediate as both relations are $\tau$ and output normal bisimulations.
%\paragraph{Case $\alpha = a(x)$.}
suppose $P \arr {a(x)} P'$. 
%$P\sub {\out {m_1} \nil} {x_1}  \simNOR Q\sub {\out {m_1} \nil} {x_1}$.
Now, if $P \arr {a(x)} P'$ then  also 
$P\{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \}$ 
must be capable of performing  such an action, so that 
\[
P\{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \}
\arr {a(x)} P'\{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \}\] 
exists. In turn, by definition of $\simNOR$, such an action guarantees that there exists a $Q'$ that 
%$\begin{itemize}
%\item 
matches that input action, i.e. 
\[
Q\{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \}
\arr {a(x)} Q'\{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \};
\]
with 
%\item 
\[ 
P'\{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \}\sub {\out {m} \nil} {x} \simNOR 
Q'\{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \}\sub {\out {m} \nil} {x}.
\]
%\end{itemize}
Again, by using the definition the $\simNORex$ on the above facts, 
it is easy to see that there is a $Q'$ such that $Q \arr {a(x)} Q'$ and $P' \simNORex Q'$, and we are done.
%\as{If it's easy, it needs to be detailed. I would define a candidate relation (that closes a process using fresh outputs, as suggested), and show that it coincides with $\simNORex$. I would then relate transitions of processes and closed processes (the previous ``it is easy to see'').}

The last thing to consider are those variables in evaluation context in the open processes.
This is straightforward by noting that by definition of $\simNORex$, all such variables have been closed with a trigger.
So, suppose  $P \simNORex Q$ and 
\[
P\{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil} x \}  \equiv \out {m_1} \nil \parallel P' \{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}}\}
\]
where $m_1$ is fresh. 
We need to show that $Q$ has a similar structure, i.e. that $Q \equiv x \parallel Q'$, with $P ' \simNORex Q'$.
$P$ can perform an output action on $m_1$, thus evolving to 
$P' \{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \}$.
%, where $m'$ is a fresh name (obtained from the definition of $\simNORex$ for output actions).
By definition of $\simNORex$, $Q$ can match this action,
and evolves to some process %$Q_0 \equiv m'.\nil \parallel 
$Q^*$, 
%$P' \{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \} \parallel m'.\nil$ which is $\simNORex$-bisimilar to 
with $m'.\nil \parallel P' \{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \} \simNORex  m'.\nil  \parallel Q^*$, where $m'$ is a fresh name (obtained from the definition of $\simNORex$ for output actions).
%\as{No! This create a new trigger $\inpC m . \nil$ on the $P$ side, and it needs to be taken into account}. 
The input on $m'$ can be trivially consumed on both sides, and one has 
$P' \{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \} \simNORex Q^*$.
At this point, since $m_1$ is a fresh name, we know that 
$Q$ involves a variable in evaluation context. Furthermore, since there is a correspondence between $P'$ and $Q^*$, 
they should involve substitutions in the very same fresh names.
%\as{I did not understand this last point ``involve substitutions in the very same fresh names''}. 
More precisely, we have that there should be a $Q'$ such that 
\[
Q \equiv \out {m_1} \nil \parallel Q'\{\suba {\out {m_{1}} \nil}  {x_{1}}, \ldots, \suba {\out {m_{n}} \nil}  {x_{n}} \} = \out {m_1} \nil \parallel Q^*
\]
%and that the ``open version'' of $Q$ is structurally congruent to $x \parallel Q'$, 
as desired.
%The last thing to consider is when $P \simNOR Q$ and $P \equiv a(x).(x \parallel P')$. We need to show 
%that $Q \equiv a(x).(x \parallel Q')$ and that $P' \simNOR Q'$. 
%Notice that $P$ can do an input action on $a$, 
%evolving to $\out m \nil \parallel P' \sub {\out m \nil} x$, 
%and then an output on the fresh name $m$, leading to $P' \sub {\out m \nil} x$. 
%Since $P \simNOR Q$, $Q$ must also be able of doing the same input and output actions. 
%First, it must be the case that 
%$Q \arr {a(x)} Q''\sub {\out m \nil} x$. We have that $Q''\sub {\out m \nil} x$ should do an output 
%on the fresh name $m$, which allows us to infer that $Q'' \equiv x \parallel Q'$, for some $Q'$. After that output, 
%%we end up with the process $Q'\sub {\out m \nil} x$. As a consequence, $P'\sub {\out m \nil} x \simNOR Q'\sub {\out m \nil} x$.
\end{proof}
 

\begin{lemma}
\label{l:NORo_IOo}
$\simNORo$ implies $\simIOo$.
\end{lemma}
\begin{proof}
The only difference between the bisimilarities is their output clause: they are both open bisimulations. We analyze directly the case for output action.
Suppose 
$P \simNORo Q$ and $P \arr {\out a {P''}} P'$; 
we need to show a matching action from $Q$. 
By definition of $\simNORo$, if $P \arr{\out a {P''}} P'$ then also $Q \arr{ \out a { Q''}} Q'$, with 
$m.P'' \parallel P' \simNORo m.Q'' \parallel Q'$. 
Using this and Lemma \ref{l:nor_deco} we conclude that $P'' \simNORo Q''$ and $P' \simNORo Q'$.
\end{proof}
}{
\begin{proof}[Proof (Sketch)] 
We get $P_2 \simNORo Q_2$ by maintaining the prefix at $m$, 
and 
thus
%therefore 
preventing runs of 
%the 
processes $P_1$ and $Q_1$.  
 
We can also consume entirely the processes $P_2$ and $Q_2$ (by observing only 
their  inputs or outputs), then consume prefix $m$; we are  thus left 
with  $P_1$ and $Q_1$, which should therefore be bisimilar. 
\end{proof}
}
%%%% END IF LONG 6
 
\begin{lemma}
\label{l:NorConHO} 
In  $\PrOp$, relations $\simHO$, $\simNORo$ and $\simCON$ coincide.
\end{lemma}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  #8
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\iflong
{\begin{proof}[Proof] 
This is an immediate consequence of previous results. In fact, we have proved 
(on open processes) the following implications: 
\begin{enumerate}
\item $\simIOo $ implies $\simHO$ (Corollary~\ref{c:HO_IOo}).  
\item $\simHO $ implies $\simCON$ (Lemma \ref{l:HO_CON});  
\item $\simCON $ implies $\simNOR$ (Lemma \ref{l:CON_NOR});
\item $\simNOR$ implies $\simNORo$ (Lemma~\ref{l:norOpCl});
\item $\simNORo $ implies $\simIOo$ (Lemma~\ref{l:NORo_IOo}).
\end{enumerate}
\end{proof}  
}{
\begin{proof}[Proof (Sketch)] 
One shows the following implications (on open processes): 
$\simHO $ implies $\simCON$ 
(this is essentially a consequence of the  congruence of $\simHO$);  
$\simCON $ implies $\simNOR$; 
$\simNOR$ implies $\simNORo$; 
 $\simNORo $ implies $\simIOo$ (here  we use 
   Lemma~\ref{l:nor_deco}).
$\simIOo $ implies $\simHO$ (Corollary~\ref{c:HO_IOo}).  
\end{proof}}

We then extend the result to all complete combinations of the
\ahopi\ bisimulation clauses (Definitions~\ref{d:cla_op} and \ref{d:cla_clo}).
 
\begin{theorem}
\label{t:all}
All complete combinations of the \ahopi\ bisimulation clauses
coincide, and are decidable.  
\end{theorem} 
\iflong{}{
\begin{proof}[Proof (Sketch)]
In Lemma~\ref{l:NorConHO} we have proved that 
the  
 least demanding combination  
 ($\simIOo$) coincides with the
 most demanding ones ($\simHO$ and $\simCON$). Decidability then follows from Lemma \ref{l:decIOo}.
\end{proof} 
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  #9
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
\iflong
{\begin{proof}
In Lemma~\ref{l:NorConHO} we have proved that 
the  
 least demanding combination  
 ($\simIOo$) coincides with the
 most demanding ones ($\simHO$ and $\simCON$). Decidability then follows from Lemma \ref{l:decIOo}.
\end{proof} 

We find this ``collapsing'' of bisimilarities in \ahopi significant; 
the only similar result we are aware of is by \cite{Cao06}, who showed 
that 
strong context bisimulation and strong normal bisimulation coincide in
higher-order $\pi$-calculus.
}{}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



%\finish{point out that also environmental bisimilarity coincide (it is
%similar to closed output normal bisimulation, in fact)} 

\iflong{\section{Barbed Congruence and Asynchronous Equivalences}\label{s:barbed}}{\Section{Barbed Congruence and Asynchronous Equivalences}\label{s:barbed}}


We now show that the labeled bisimilarities of
Section~\ref{s:bism} coincide with \emph{barbed congruence}, the form
of  
contextual equivalence  used in concurrency to justify 
bisimulation-like relations.
%\iflong{}{ (proof sketches are in Appendix \ref{a:barbed})}.   
Below 
%``barbed congruence'' is actually  
%its 
we use \emph{reduction-closed} barbed congruence \citep{HoYo95,SaWabook}, as this makes
some technical details simpler; however the results also hold for
ordinary barbed congruence \citep{MiSa92}. 
It is worth recalling that the main difference between reduction-closed and ordinary barbed 
congruence is quantification over contexts (see (2) in Definition \ref{d:abco} below).
More importantly, we consider the \emph{asynchronous} version of
barbed congruence, where barbs are only produced by   output messages; in 
synchronous barbed congruence  inputs may also  contribute.
We use the asynchronous version for two reasons.
First, asynchronous barbed congruence is a weaker relation, which makes
the results stronger (they imply the corresponding results for 
the  synchronous relation). 
Second, 
asynchronous barbed congruence is more natural in 
\ahopi\ because it is an asynchronous calculus --- 
it has no output prefix.


Note also that the labeled bisimilarities of Section~\ref{s:bism}
have been defined in the synchronous style. 
In an \emph{asynchronous labeled bisimilarity}  (see, e.g.,  \citep{AmadioCS98})
the input clause is weakened so as to allow, in certain conditions, an
input action to be matched also by  a $\tau$-action.  
For instance, %the input clause of 
input normal bisimulation (Definition \ref{d:cla_clo}(2)) would
become: %\as{This seems clearly wrong: don't we need to substitute $\out{a}{\out m \nil}$ in $P'$ for the second case?}
% Not really, the output on a is intended to compensate for the fact P did only an input while Q did a tau (i.e. both output and input).
\begin{itemize}
\item if $ P \arr{\inp a x}  {P'}$ then, for some fresh name $m$,

\begin{enumerate}
\item either $Q \arr{\inp a x} Q'$ and
${P'} \sub {\out m\nil}x
\RR{Q'}\sub {\out m\nil}x$; %, where $m$ is fresh;

\item or $Q \arr{\tau} Q'$ and $P'\sub {\out m\nil}x \RR Q' \parallel \out{a}{\out m\nil}$.

\end{enumerate}
\end{itemize}



We now define asynchronous barbed congruence.
We write 
$P \dwa_{\overline a}$ (resp.\ $P \dwa_{ a}$) if $P$ can perform an
output (resp.\ input) transition at $a$. 

\begin{mydefi}
\label{d:abco}
\iflong{
\emph{Asynchronous barbed congruence}, 
$\sbc$, is the largest symmetric relation on closed processes 
that is
\begin{enumerate}
\item a $\tau$-bisimulation (Definition~\ref{d:cla_op}(1));
\item context-closed (i.e.,  $P \sbc Q$  implies    $\ct P\sbc \ct Q$, for all closed contexts $\ct \cdot$); 
\item barb preserving (i.e., if $P \sbc Q$  %for $P,Q$ closed,
and  $P \dwa_{\overline a}$, then also  $Q\dwa_{\overline a}$).
\end{enumerate}
}{
\emph{Asynchronous barbed congruence}, 
$\sbc$, is the largest relation on closed processes 
that is
symmetric, 
is   a $\tau$-bisimulation (Definition~\ref{d:cla_op}(1)),
context-closed 
(i.e.,  $P \sbc Q$  implies    $\ct P\sbc \ct Q$, for all closed contexts $\ct \cdot$), and barb preserving 
(i.e., if $P \sbc Q$  %for $P,Q$ closed,
and  $P \dwa_{\overline a}$, then also  $Q\dwa_{\overline a}$).
}
\end{mydefi}

In \emph{synchronous} barbed congruence, input barbs $P \dwa_a$ are also
observable. % (in the ``barb preserving'' condition).

\begin{lemma}
\label{l:abc}
Asynchronous  barbed congruence coincides with normal bisimilarity.
\end{lemma} 

\iflong
{
\begin{proof}
We first show that $\simNOR$ implies $\sbc$, and then its converse, which is harder.
The relation $\simNOR$ satisfies the 
conditions in Definition \ref{d:abco} as follows.
First, both relations are $\tau$-bisimulations so condition (1) above
trivially holds. Second, 
the context-closure condition %(i.e. if $P \RR Q$ then $\ct P \RR \ct Q$.) 
follows from the fact that $\simNOR$ is a congruence.
Finally, 
the barb-preserving condition is seen to hold 
by definition of $\simNOR$: having 
$P \simNOR Q$
implies that an output action 
of $P$ on $a$ has to be matched by an output action of $Q$ on $a$; hence, we have that 
if $P \dwa_{\overline a}$, then also  $Q\dwa_{\overline a}$.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


Now the converse. We show that relation $\sbc$ satisfies the three conditions for $\simNOR$ in Definition \ref{d:bisimulations}.
Suppose $P \sbc Q$ and $P \arr \alpha P'$; we have to show a matching transition $Q \arr \alpha Q'$.
We proceed by a  case analysis on the form $\alpha$ can take. 

\paragraph{Case $\alpha = \tau$}
Since by definition $\sbc$ is a $\tau$-bisimulation, then 
there is a $Q'$ such that $Q \arr \tau Q'$ and $P' \sbc Q'$ and we are done.

\paragraph{Case $\alpha = \out a {P''}$}
We have $P \arr{\out a {P''}} P'$: it can be shown that 
$\sbc$ is an output normal bisimulation by showing a suitable context. 
Let $\ctii{\ccc{o}}{a}{\cdot}$ be the context
\[
\ctii{\ccc{o}}{a}{\cdot} = \holE \parallel a(x).(m.x \parallel \overline{n} \parallel n . \nil) 
\]
where $m,n$ are fresh names. We then have $\ctii{\ccc{o}}{a}{P} \arr \tau P_1$ with $P_1 \dwa_{\overline{n}}$. 
Indeed, we have $P_1 \equiv P' \parallel m.P'' \parallel \overline{n} \parallel n . \nil$.
By definition of $\sbc$, we have also $\ctii{\ccc{o}}{a}{Q} \arr \tau Q_1$ and necessarily, $Q_1 \dwa_{\overline{n}}$. 
Since $n$ is a fresh name, 
we infer that $Q$ also has an output on $a$, such that 
$Q \arr {\out a {Q''}} Q'$ and hence $Q_1 \equiv Q' \parallel m.Q'' \parallel \overline{n} \parallel n . \nil$. 
Note that $(P_1, Q_1)$ is in $\sbc$. 
They can consume the actions on $n$; since it is a fresh name, only the corresponding $\tau$ action of $Q_1$ can match it. %performed by $P_1$. 
As a result, both processes evolve to processes 
$ P' \parallel m.P''$ and $Q' \parallel m.Q''$ that are still in $\sbc$.
We then conclude that $\sbc$ is an output normal bisimulation.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\paragraph{Case $\alpha = a(x)$}
We have $P \arr{a(x)} P'$. 
Again, to show that $\sbc$ is an input normal bisimulation, we define a suitable context.
Here, the asynchronous nature of \ahopi (more precisely, 
the lack of output prefixes, which prevents the 
control of output actions by  modifying their continuation)
and the input clause for $\simNOR$ it induces
(reported above) result in a more involved definition of these contexts. 
Notice that simply 
defining a context with an output action on $a$ so as to force synchronization with the input action
does not work here: process $P$ itself could contain other 
output actions on $a$ that could synchronize with the input we are interested in, and as output actions have no continuation, it is not possible to put a fresh barb indicating it has been consumed.
We overcome this difficulty by (i) renaming {\em every output} in $P$, so as to avoid the possibility of $\tau$ actions 
(including those coming from synchronizations on channels different from $a$),
(ii) consuming the input action on $a$ (by placing the renamed process in a suitable context) 
and then (iii) restoring the initial outputs.


We define a context for (i) above, i.e., to rename every output in a process so as to prevent $\tau$ actions. 
We start by denoting by 
$out(P)$ the multiset of names in output subject position in a process $P$.
Further, let $\sigma$ denote an injective relation between each occurrence of name in $out(P)$ and a fresh name.
Let $\ct \cdot$ be the context
\[
\cti{}{\cdot} = \holE \parallel \prod_{(b_i,c_i) \in \sigma} b_i(x).\out{c_i}{x}
\]
which uniquely renames every output $\out {b_i} {S_i}$ as $\out {c_i} {S_i}$.
(We shall use $c_i$ ($i \in 1..n$) to denote the fresh names for the renamed outputs.)
Consider now processes $\cti{}{P}$ and  $\cti{}{Q}$:
since the renaming is on fresh channels, it can be ensured that the $\tau$ action due to the renaming of one output on one process
is matched by the other process with a $\tau$ action that corresponds to the renaming of the same output.
At the end, after a series of $n$ $\tau$ actions, $\cti{}{P}$ and  $\cti{}{Q}$
become 
processes $P_1$ and $Q_1$ that have no $\tau$ actions arising from their subprocesses and that are in $\sbc$.
%Note also that $P_1 \sbc Q_1$: each $\tau$ action produced by renaming a single output in a process can be matched by the other.
At this point it is then possible to use a context for (ii), to 
capture the input action on $a$ in $P_1$. Let $\ctii{\ccc{i}}{a}{\cdot}$ be the context 
\[
\ctii{\ccc{i}}{a}{\cdot} = \holE \parallel \out{a}{\out m \nil} 
\]
where $m$ is a fresh name. 
We then have 
\[
\ctii{\ccc{i}}{a}{P_1} \arr \tau \out {c_1} {S_1} \parallel \cdots \parallel \out {c_n} {S_n} \parallel P_a \sub {\out m\nil}x \parallel P'' = P_2
\]
which, by definition of $\sbc$, implies that also it must be the case that, 
for some process $Q_2$,  $\ctii{\ccc{i}}{a}{Q_1} \arr \tau Q_2$.
In fact, since there is a synchronization at $a$, it implies that $Q_1$ must have at least one input action on $a$. 
More precisely, we have 
\[
Q_2 \equiv \out {c_1} {S_1} \parallel \cdots \parallel \out {c_n} {S_n} \parallel Q_a \sub {\out m\nil}x \parallel Q''.
\]
We notice that $P_2$ and $Q_2$ are still in $\sbc$; it remains however to perform (iii), i.e. to revert the
renaming made by $\ct \cdot$.  
To do so, we proceed analogously as before and define the context
\[
C'\holE = \holE \parallel \prod_{(c_i,b_i) \in \sigma^{-1}} c_i(x).\out{b_i}{x}.
\]
We have that each of $C'\brac{P_2}$ and  $C'\brac{Q_2}$ produces
$n$ $\tau$ steps that exactly revert the renaming done by context $C \holE$ above and lead to $P_3$ and $Q_3$, respectively. This renaming occur in lockstep (and no other $\tau$ action may be performed by $Q_2$), as each one removes a barb on a fresh name, thus the other process has to remove the same barb by doing the renaming.
Hence, $P_3$ and $Q_3$ have the same output actions as the initial $P$ and $Q$. 
To conclude, it is worth remarking that $\ctii{\ccc{i}}{a}{P} \arr \tau P_3$ in one step.
Indeed, we have 
\[ \ctii{\ccc{i}}{a}{P} \equiv T \parallel a(x).P_a \parallel P'' \parallel \out{a}{\out m \nil} \arr \tau P_3 = P' \sub {\out m \nil} x\]
where $T$ stands for all the output actions in $P$ (on which the renaming took place). 
By doing and undoing the renaming on every output, we were able to infer that
$Q$ has an analogous structure
$$ \ctii{\ccc{i}}{a}{Q} \equiv T' \parallel a(x).Q_a \parallel Q'' \parallel \out{a}{\out m \nil} \arr \tau Q_3$$
where $T'$ stands for all the output actions in $Q$.
%In fact, this is clear by noting that we have cared to do a precise renaming on outputs and to undo it appropriately.
%Since we proceeded similarly for $Q$, we have also conclude that $\ctii{\ccc{i}}{a}{Q}  \arr \tau Q_3$. 
From the definition of $\sbc$ we know it is a $\tau$-bisimulation, and then we have $P_3 \sbc Q_3$.
Let $Q' = T' \parallel Q_a \parallel Q''$, we then have $Q \arr{a(x)} Q'$ and $Q_3 = Q' \sub {\out m \nil} x$.
To summarize, we have $P \arr{a(x)} P'$, $Q \arr{a(x)} Q'$, and $P' \sub {\out m \nil} x \sbc Q' \sub {\out m \nil} x$ with $m$ fresh.
Hence we conclude that $\sbc$ is an input normal bisimulation.
\end{proof}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


}{
\begin{proof}[Proof (Sketch)]
As we are comparing a synchronous relation against an
asynchronous one,
some details of
the proof  differ  from  proofs  in the literature involving barbed
congruences.
Specifically, we have to show that two asynchronous  barbed
congruent processes $P$ and $Q$ satisfy the synchronous clause for input
transitions as by Definition~\ref{d:cla_clo}(2). To this end, 
for every message $\out a R$ that appears at top level in $P$ or $Q$,  we add a process $\inp a y. \out b y$
that renames this message to
message $\out b R$, where $b$ is some fresh channel. The resulting processes $P \parallel T$ and $Q \parallel T$ are still asynchronous barbed congruent, and as the channels $b$ are fresh, 
%any renaming of one message by a $\tau$ action 
any $\tau$ action generated by the renaming of one message 
is 
matched by a $\tau$ action from a similar renaming by the other process, 
yielding eventually two asynchronous barbed congruent processes $P' $ and $Q'$
 that cannot immediately perform  any $\tau$-transitions.
Therefore on these processes the 
$\tau$-transitions that appear in the input clause of asynchronous
bisimilarity (and which make the difference w.r.t.\ synchronous
bisimilarity) are impossible. Thus we can show that,  on such special
asynchronous processes,  any input from
$P'$ is matched by an input from $Q'$ and conversely, as in 
synchronous bisimilarities.
Finally, reverting the renaming we are able to derive an analogous
match on inputs for $P$ and $Q$.
\end{proof}
}

\begin{remark}
\label{r:} 
\iflong{
The proof relies on the fact that \ahopi\ has no operators of
recursion, choice, and restriction. 
In fact, recursion would break the proof as there could be an infinite number of
outputs to rename. Also, choice would prevent the renaming to be reversible, and 
restriction would prevent the renaming using a context as some names may be hidden. 
The higher-order aspect of \ahopi\ does not really play a role. 
The proof could indeed be adapted 
to CCS-like, or $\pi$-calculus-like, languages in which the same operators  are missing. 
}{The proof relies on the fact that \ahopi\ has no operators of
recursion, choice, and restriction. The higher-order aspect of \ahopi\ does
not really play a role. 
The proof could indeed be adapted
to CCS-like, or $\pi$-calculus-like, languages in which the same
operators  are missing. 
}
\end{remark}





\begin{corollary}
\label{c:all2}
In \ahopi\ asynchronous and synchronous barbed congruence coincide,
and they also coincide with all 
complete combinations of the \ahopi\ bisimulation clauses
of Theorem~\ref{t:all}.  
\end{corollary}

Further, Corollary~\ref{c:all2} can be extended to include 
the asynchronous
versions of the labeled bisimilarities in Section~\ref{s:bism}
(precisely, the \emph{complete asynchronous combinations} of the \ahopi\ bisimulation
clauses; that is, complete combinations that make use of an asynchronous
input clause as outlined before Definition~\ref{d:abco}).
This holds because:
(i) all proofs of Section \ref{s:bism} can be easily adapted to   
the corresponding  asynchronous labeled  bisimilarities; (ii)
using standard reasoning for barbed congruences, one can show 
that asynchronous normal bisimilarity coincides with asynchronous
barbed congruence; (iii)   via Corollary~\ref{c:all2} one can then
relate the asynchronous labeled bisimilarities to the synchronous
ones.


%\finish{above: check again details}


